|
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'') that describe the meanings of expressions from the languages. Other approaches to providing formal semantics of programming languages include axiomatic semantics and operational semantics. Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, programs (or program phrases) might be represented by partial functions or by games between the environment and the system. An important tenet of denotational semantics is that ''semantics should be compositional'': the denotation of a program phrase should be built out of the denotations of its subphrases. ==Historical development== Denotational semantics originated in the work of Christopher Strachey and Dana Scott in the late 1960s.〔Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.〕 As originally developed by Strachey and Scott, denotational semantics provided the denotation (meaning) of a computer program as a function that mapped input into output.〔Dana Scott and Christopher Strachey. ''Toward a mathematical semantics for computer languages'' Oxford Programming Research Group Technical Monograph. PRG-6. 1971.〕 To give denotations to recursively defined programs, Scott proposed working with continuous functions between domains, specifically complete partial orders. As described below, work has continued in investigating appropriate denotational semantics for aspects of programming languages such as sequentiality, concurrency, non-determinism and local state. Denotational semantics have been developed for modern programming languages that use capabilities like concurrency and exceptions, e.g., Concurrent ML,〔John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, ''Lecture Notes in Computer Science'', Vol. 693. 1993〕 CSP,〔A. W. Roscoe. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.〕 and Haskell.〔Simon Peyton Jones, Alastair Reid, Fergus Henderson, Tony Hoare, and Simon Marlow. "A semantics for imprecise exceptions" Conference on Programming Language Design and Implementation. 1999.〕 The semantics of these languages is compositional in that the denotation of a phrase depends on the denotations of its subphrases. For example, the meaning of the applicative expression f(E1,E2) is defined in terms of semantics of its subphrases f, E1 and E2. In a modern programming language, E1 and E2 can be evaluated concurrently and the execution of one of them might affect the other by interacting through shared objects causing their denotations to be defined in terms of each other. Also, E1 or E2 might throw an exception which could terminate the execution of the other one. The sections below describe special cases of the semantics of these modern programming languages. 抄文引用元・出典: フリー百科事典『 ウィキペディア(Wikipedia)』 ■ウィキペディアで「denotational semantics」の詳細全文を読む スポンサード リンク
|